k:Knd, l:IdLnk, dt:x:Id fp Type. k  dom(lnk-decl(l;dt))  (lnk-decl(l;dt)(k) ~ dt(tag(k))) 

latex

Definitions	tag(k), x:AB(x), left+right, Knd, t  T, IdLnk, Id, Type, x. t(x), x:A. B(x), a:A fp B(a), lnk-decl(l;dt), x.A(x), Top, x:AB(x), KindDeq, x  dom(f), b, P  Q, {T}, SQType(T), s = t, Prop, s ~ t, False, A, b, , IdDeq, rcv(l,tg), P & Q, P  Q, Unit, f(x)?z, Void
Lemmas	lnk-decl-dom-not, lnk-decl-cap, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, rcv wf, id-deq wf, bool wf, bnot wf, not wf, lnk-decl-dom2, IdLnk sq, lnk-decl-dom, assert wf, fpf-dom wf, Kind-deq wf, fpf-trivial-subtype-top, lnk-decl wf, fpf wf, Id wf, IdLnk wf, Knd wf